;;;============================================================
;;;
;;; Subject: EAT General Properties
;;;
;;;------------------------------------------------------------
;;;
;;; Jónathan Heras Vicente
;;; Date: 28-10-09
;;;
;;;============================================================

#| Certification code:

(certify-book "eat-general-properties" 0 nil)

|#


(in-package "ACL2")

(include-book "dg-list")

(set-verify-guards-eagerness 0)



;;;============================================================================
;;;
;;; EAT definitions
;;;
;;;============================================================================

;;;   The original EAT definitions are the following:

#|

(DEFUN CMP-D-LS (d ls)
  (declare (type fixnum+ d) (type list ls))
  (do ((p ls (cdr p))
       (rsl empty-list (let ((j (car p)))
                         (cons (cond ((< d j) (1- j))
                                     (t (decf d) j))
                               rsl))))
      ((endp p) (values (nreverse rsl) d))
    (declare (type list p rsl))
    (when (<= 0 (- d (car p)) 1)
      (return (values (nreconc rsl (rest p)) nil)))))



; (cmp-d-ls 6 '(4 3 2))     => (4 3 2) 3
; (cmp-d-ls 0 '(4 3 2))     => (3 2 1) 0
; (cmp-d-ls 3 '(6 5 2 0))   => (5 4 0) nil
; (cmp-d-ls 3 '(6 4 0))     => (5 3 0) 2
; (cmp-d-ls 3 '(6 3 0))     => (5 0) nil
; (cmp-d-ls 3 '(6 2 0))     => (5 0) nil

|#

;;;   We translate these functions to ACL2 as follows:

(defun cmp-d-ls-dgop-do (d p rsl)
  (cond ((endp p) (reverse rsl))
        ((< d (car p)) (cmp-d-ls-dgop-do d (cdr p) (cons (1- (car p)) rsl)))
        ((and (<= 0 (- d (car p)))
              (<= (- d (car p)) 1)) (append (reverse rsl) (rest p)))
        (t (cmp-d-ls-dgop-do (1- d) (cdr p) (cons (car p) rsl)))
        )
  )

(defun cmp-d-ls-d-do (d p)
  (cond ((endp p) d)
	((< d (car p)) (cmp-d-ls-d-do d (cdr p) ))
        ((and (<= 0 (- d (car p)))
              (<= (- d (car p)) 1)) nil)
        (t (cmp-d-ls-d-do (1- d) (cdr p)))
        )
  )

(defun cmp-d-ls (d ls)
  (cmp-d-ls-dgop-do d ls nil)
  )

;;;----------------------------------------------------------------------------
;;;
;;; New recursive schemata of these functions
;;;
;;;----------------------------------------------------------------------------

(encapsulate
 ()
 
 (local
  (defthm append-revappend
      (equal (append (revappend l1 l2) l3)
             (revappend l1 (append l2 l3)))))
 
 (local
  (defthm revappend-append
      (equal (revappend (append ls1 ls2) ls3)
             (revappend ls2 (revappend ls1 ls3)))))
 
 (local
  (defthm cmp-d-ls-dgop-do-append-rsl
      (implies (and (true-listp rsl1)
                    (true-listp rsl2))
               (equal (cmp-d-ls-dgop-do s p (append rsl1 rsl2))
                      (append (reverse rsl2) (cmp-d-ls-dgop-do s p rsl1))))
    :rule-classes nil))
 
 (local
  (defthm cmp-d-ls-dgop-do-nil-rsl
      (implies (and (true-listp rsl1)
                    (not (endp rsl1)))
               (equal (cmp-d-ls-dgop-do s p rsl1)
                      (append (reverse rsl1) (cmp-d-ls-dgop-do s p nil))))
    :hints (("Goal" :use (:instance cmp-d-ls-dgop-do-append-rsl
                                    (rsl1 nil)
                                    (rsl2 rsl1))))))
 
 (defthm cmp-d-ls-recursive
     (equal (cmp-d-ls d ls)
            (cond ((endp ls) nil)
                  ((< d (car ls)) (cons (1- (car ls)) (cmp-d-ls d (cdr ls))))
                  ((and (<= 0 (- d (car ls)))
                        (<= (- d (car ls)) 1)) (cdr ls))              
                  (t (cons (car ls) (cmp-d-ls (1- d) (cdr ls))))
                  ))
   :rule-classes :definition)
 
 (defun cmp-d-ls-induct (d ls)
   (cond 
	 ((endp ls) nil)
         ((< d (car ls)) (cons (1- (car ls)) (cmp-d-ls-induct d (cdr ls))))
         ((and (<= 0 (- d (car ls)))
               (<= (- d (car ls)) 1)) (cdr ls))              
         (t (cons (car ls) (cmp-d-ls-induct (- d 1) (cdr ls))))
         )
   )
 
 (in-theory (disable cmp-d-ls))
 
 )

(defthm cmp-d-ls-cmp-d-ls-induct
    (equal (cmp-d-ls i ls)
           (cmp-d-ls-induct i ls)))

;; Notar que si > j (1+ (car ls)) entonces cmp-d-ls-induct j ls es ls

(defthm cmp-d-induct-cmp-d-induct-case-1.3-help1
  (implies (and (natp j) (dgl-p ls)
		(> j (+ (car ls) 1))
		(not (endp ls))
		) 
	   (equal (cmp-d-ls-induct j ls)
		  ls)))

(defthm cmp-d-induct-cmp-d-induct-case-1.3-help2
  (implies (and (natp j) (dgl-p ls)
		(>=  j (car ls))
		(not (endp ls))
		(not (and (<= 0 (- j (car ls)))
			  (<= (- j (car ls)) 1)))
		) 
	   (equal (cmp-d-ls-induct j ls)
		  ls)))

(defthm cmp-d-ls-d-do-not-nil
  (implies (and (natp j) 
		(dgl-p ls)
		(> j (+ (car ls) 1))
		(not (endp ls))
		) 
	   (cmp-d-ls-d-do j ls)))


(defthm cmp-d-induct-cmp-d-induct-case-1.3-help1-bis
  (implies (and (natp j) (dgl-p ls)
		(> j (+ (car ls) 1))
		(not (endp ls))
		) 
	   (equal (cmp-d-ls-d-do j ls)
		  (- j (len ls)))))

(defthm cmp-d-induct-cmp-d-induct-case-1.3-help2-bis
  (implies (and (natp j) (dgl-p ls)
		(>=  j (car ls))
		(not (endp ls))
		(not (and (<= 0 (- j (car ls)))
			  (<= (- j (car ls)) 1)))
		) 
	   (equal (cmp-d-ls-d-do j ls)
		  (- j (len ls)))))



;;;----------------------------------------------------------------------------
;;;
;;; Domain properties
;;;
;;;----------------------------------------------------------------------------

(defthm dgl-p-cmp-d-ls
    (implies (and (dgl-p dgl)
                  (natp n))
             (dgl-p (cmp-d-ls n dgl)))
  :hints (("Goal" :induct (cmp-d-ls-induct n dgl))))




;;;----------------------------------------------------------------------------
;;;
;;; face o deg forall  i < j 
;;; Property 3 of Simplicial Sets for degeneration lists
;;;
;;;----------------------------------------------------------------------------


;; First, I prove that the inductive versions of cmp-d-ls and cmp-s-ls satisfy the
;; property

(defthm cmp-d-ls-induct-cmp-s-ls-induct
    (implies (and (< i j) (dgl-p ls))
             (equal (cmp-d-ls-induct i (cmp-s-ls-induct j ls))
                    (cmp-s-ls-induct (- j 1) (cmp-d-ls-induct i ls)
                                     ))))

(defthm cmp-s-ls-cmp-s-ls-induct
    (equal (cmp-s-ls i ls)
           (cmp-s-ls-induct i ls)))

(defthm cmp-d-ls-induct-cmp-s-ls
    (implies (and (< i j) (dgl-p ls))
             (equal (cmp-d-ls-induct i (cmp-s-ls j ls))
                    (cmp-s-ls (- j 1) (cmp-d-ls-induct i ls)
                              ))))


;; The non inductive versions also satisfy the property

(defthm cmp-d-ls-cmp-s-ls
    (implies (and (< i j) (dgl-p ls))
             (equal (cmp-d-ls i (cmp-s-ls j ls))
                    (cmp-s-ls (- j 1) (cmp-d-ls i ls)
                              ))))



;;;----------------------------------------------------------------------------
;;;
;;; face o deg forall  i 
;;; Property 4 of Simplicial Sets for degeneration lists
;;;
;;;----------------------------------------------------------------------------

(defthm cmp-d-ls-case-induct
    (implies (and (not (endp ls))
                  (< j (car ls)))
             (equal (cmp-d-ls-induct j ls)
                    (cons (1- (car ls)) (cmp-d-ls-induct j (cdr ls))))))


(defthm cmp-d-ls-induct-cmp-s-ls-induct-2-a
    (implies (dgl-p ls)
             (equal (cmp-d-ls-induct i (cmp-s-ls-induct i ls))
                    ls)))

(defthm cmp-d-ls-induct-cmp-s-ls-induct-2-b
    (implies (and (natp i) (dgl-p ls))
             (equal (cmp-d-ls-induct (+ i 1) (cmp-s-ls-induct i ls))
                    ls)))

(defthm cmp-d-ls-induct-cmp-s-ls-induct-2
    (implies (and (natp i) (dgl-p ls))
             (equal (cmp-d-ls-induct i (cmp-s-ls-induct i ls))
                    (cmp-d-ls-induct (+ i 1) (cmp-s-ls-induct i ls))
                    ))
  )

(defthm cmp-d-ls-cmp-s-ls-property-4-a
    (implies (and (natp i) (dgl-p ls))
             (equal (cmp-d-ls i (cmp-s-ls i ls))
                    (cmp-d-ls (+ i 1) (cmp-s-ls i ls)
                              ))))

(defthm cmp-d-ls-cmp-s-ls-property-4-b
    (implies (and (natp i) (dgl-p ls))
             (equal (cmp-d-ls i (cmp-s-ls i ls))
                    ls)))

(defthm cmp-d-ls-cmp-s-ls-property-4-c
    (implies (and (natp i) (dgl-p ls))
             (equal (cmp-d-ls (+ i 1) (cmp-s-ls i ls))
		    ls)))






;;;----------------------------------------------------------------------------
;;;
;;; face o deg forall  i > j+1
;;; Property 5 of Simplicial Sets for degeneration lists 
;;;
;;;----------------------------------------------------------------------------

(defthm cmp-d-ls-induct-cmp-s-ls-induct-3-case4
    (implies (and (> i (+ j 1)) (dgl-p ls) (endp ls))
             (equal (cmp-d-ls-induct i (cmp-s-ls-induct j ls))
		    (cmp-s-ls-induct j (cmp-d-ls-induct (- i 1) ls))
                                     )))


(defthm cmp-d-ls-induct-cmp-s-ls-induct-3-case3
    (implies (and (> i (+ j 1)) (dgl-p ls) (not (endp ls)) (natp i)
		  (natp j)
		  (< (- i 1) (car ls))
		  (equal (cmp-d-ls-induct i (cmp-s-ls-induct j (cdr ls)))
			 (cmp-s-ls-induct j (cmp-d-ls-induct (- i 1) (cdr ls)))
                                     )
		  )
             (equal (cmp-d-ls-induct i (cmp-s-ls-induct j ls))
		    (cmp-s-ls-induct j (cmp-d-ls-induct (- i 1) ls))
                                     )))


(defthm cmp-d-ls-induct-cmp-s-ls-induct-3-case2
    (implies (and (> i (+ j 1)) (dgl-p ls) (not (endp ls)) (natp i)
		  (natp j)
		  (>= (- i 1) (car ls))
		  (and (<= 0 (- (- i 1) (car ls)))
		       (<= (- (- i 1) (car ls)) 1 ))
		  )
             (equal (cmp-d-ls-induct i (cmp-s-ls-induct j ls))
		    (cmp-s-ls-induct j (cmp-d-ls-induct (- i 1) ls))
                                     )))



(defthm cmp-d-ls-induct-cmp-s-ls-induct-3-case1-a
    (implies (and (> i (+ j 1)) (dgl-p ls) (not (endp ls)) (natp i)
		  (natp j)
		  (>= (- i 1) (car ls))
		  (not (<= 0 (- (- i 1) (car ls))))
		  (equal (cmp-d-ls-induct (- i 1) (cmp-s-ls-induct j (cdr ls)))
			 (cmp-s-ls-induct j (cmp-d-ls-induct (- i 2) (cdr ls)))
                                     )
		  )
             (equal (cmp-d-ls-induct i (cmp-s-ls-induct j ls))
		    (cmp-s-ls-induct j (cmp-d-ls-induct (- i 1) ls))
                                     )))


(defthm cmp-d-ls-induct-cmp-s-ls-induct-3-case1-b/1
    (implies (and (> i (+ j 1)) (dgl-p ls) (not (endp ls)) (natp i)
		  (natp j)
		  (>= (- i 1) (car ls))
		  (not (<= (- (- i 1) (car ls)) 1))
		  (< (car ls) j)
		  (equal (cmp-d-ls-induct (- i 1) (cmp-s-ls-induct j (cdr ls)))
			 (cmp-s-ls-induct j (cmp-d-ls-induct (- i 2) (cdr ls)))
                                     )
		  )
             (equal (cmp-d-ls-induct i (cmp-s-ls-induct j ls))
		    (cmp-s-ls-induct j (cmp-d-ls-induct (- i 1) ls))
                                     )))


(defthm cmp-d-ls-induct-cmp-s-ls-induct-3-case1-b/2.1.1
    (implies (and (> i (+ j 1)) (dgl-p ls) (not (endp ls)) (natp i)
		  (natp j)
		  (>= (- i 1) (car ls))
		  (not (<= (- (- i 1) (car ls)) 1))
		  (>= (car ls) j)
		  (equal (cmp-d-ls-induct (- i 1) (cmp-s-ls-induct j (cdr ls)))
			 (cmp-s-ls-induct j (cmp-d-ls-induct (- i 2) (cdr ls)))
                                     )
		  )
             (equal (cmp-d-ls-induct i (cmp-s-ls-induct j ls))
		    (cmp-d-ls-induct i (cons (1+ (car ls)) (cmp-s-ls-induct j (cdr ls))))
                                     )))

(defthm cmp-d-ls-induct-cmp-s-ls-induct-3-case1-b/2.1
    (implies (and (> i (+ j 1)) (dgl-p ls) (not (endp ls)) (natp i)
		  (natp j)
		  (>= (- i 1) (car ls))
		  (not (<= (- (- i 1) (car ls)) 1))
		  (not (and (<= 0 (- (- i 1) (car ls)))
		       (<= (- (- i 1) (car ls)) 1 )))
		  (>= (car ls) j)
		  (equal (cmp-d-ls-induct (- i 1) (cmp-s-ls-induct j (cdr ls)))
			 (cmp-s-ls-induct j (cmp-d-ls-induct (- i 2) (cdr ls)))
                                     )
		  )
             (equal (cmp-d-ls-induct i (cmp-s-ls-induct j ls))
		    (cons (1+ (car ls)) (cmp-d-ls-induct (- i 1) (cmp-s-ls-induct j (cdr ls))))
                                     )))


(defthm cmp-d-ls-induct-cmp-s-ls-induct-3-case1-b/2.2.1
    (implies (and (> i (+ j 1)) (dgl-p ls) (not (endp ls)) (natp i)
		  (natp j)
		  (>= (- i 1) (car ls))
		  (not (<= (- (- i 1) (car ls)) 1))
		  (not (and (<= 0 (- (- i 1) (car ls)))
		       (<= (- (- i 1) (car ls)) 1 )))
		  (>= (car ls) j)
		  (equal (cmp-d-ls-induct (- i 1) (cmp-s-ls-induct j (cdr ls)))
			 (cmp-s-ls-induct j (cmp-d-ls-induct (- i 2) (cdr ls)))
                                     )
		  )
             (equal (cmp-d-ls-induct (- i 1) ls)
		    (cons (car ls) (cmp-d-ls-induct (1- (- i 1)) (cdr ls))))
                                     ))

(defthm aux 
  (implies (natp i)
	   (equal (1- (- i 1))
		  (- i 2))))

(defthm cmp-d-ls-induct-cmp-s-ls-induct-3-case1-b/2.2.2
    (implies (and (> i (+ j 1)) (dgl-p ls) (not (endp ls)) (natp i)
		  (natp j)
		  (>= (- i 1) (car ls))
		  (not (<= (- (- i 1) (car ls)) 1))
		  (not (and (<= 0 (- (- i 1) (car ls)))
		       (<= (- (- i 1) (car ls)) 1 )))
		  (>= (car ls) j)
		  (equal (cmp-d-ls-induct (- i 1) (cmp-s-ls-induct j (cdr ls)))
			 (cmp-s-ls-induct j (cmp-d-ls-induct (- i 2) (cdr ls)))
                                     )
		  )
             (equal (cmp-d-ls-induct (- i 1) ls)
		    (cons (car ls) (cmp-d-ls-induct (- i 2) (cdr ls))))
                                     ))


(defthm cmp-d-ls-induct-cmp-s-ls-induct-3-case1-b/2.2.3
    (implies (and (> i (+ j 1)) (dgl-p ls) (not (endp ls)) (natp i)
		  (natp j)
		  (>= (- i 1) (car ls))
		  (not (<= (- (- i 1) (car ls)) 1))
		  (not (and (<= 0 (- (- i 1) (car ls)))
		       (<= (- (- i 1) (car ls)) 1 )))
		  (>= (car ls) j)
		  (equal (cmp-d-ls-induct (- i 1) (cmp-s-ls-induct j (cdr ls)))
			 (cmp-s-ls-induct j (cmp-d-ls-induct (- i 2) (cdr ls)))
                                     )
		  )
             (equal (cmp-s-ls-induct j (cmp-d-ls-induct (- i 1) ls))
		    (cmp-s-ls-induct j (cons (car ls) (cmp-d-ls-induct (- i 2) (cdr ls))))
                                     )))


(defthm cmp-d-ls-induct-cmp-s-ls-induct-3-case1-b/2.2
    (implies (and (> i (+ j 1)) (dgl-p ls) (not (endp ls)) (natp i)
		  (natp j)
		  (>= (- i 1) (car ls))
		  (not (<= (- (- i 1) (car ls)) 1))
		  (not (and (<= 0 (- (- i 1) (car ls)))
		       (<= (- (- i 1) (car ls)) 1 )))
		  (>= (car ls) j)
		  (equal (cmp-d-ls-induct (- i 1) (cmp-s-ls-induct j (cdr ls)))
			 (cmp-s-ls-induct j (cmp-d-ls-induct (- i 2) (cdr ls)))
                                     )
		  )
             (equal (cmp-s-ls-induct j (cmp-d-ls-induct (- i 1) ls))
		    (cons (1+ (car ls)) (cmp-s-ls-induct j  (cmp-d-ls-induct (- i 2) (cdr ls))))
                                     )))

(defthm cmp-d-ls-induct-cmp-s-ls-induct-3-case1-b/2
    (implies (and (> i (+ j 1)) (dgl-p ls) (not (endp ls)) (natp i)
		  (natp j)
		  (>= (- i 1) (car ls))
		  (not (<= (- (- i 1) (car ls)) 1))
		  (not (and (<= 0 (- (- i 1) (car ls)))
		       (<= (- (- i 1) (car ls)) 1 )))
		  (>= (car ls) j)
		  (equal (cmp-d-ls-induct (- i 1) (cmp-s-ls-induct j (cdr ls)))
			 (cmp-s-ls-induct j (cmp-d-ls-induct (- i 2) (cdr ls)))
                                     )
		  )
             (equal (cmp-d-ls-induct i (cmp-s-ls-induct j ls))
		    (cmp-s-ls-induct j (cmp-d-ls-induct (- i 1) ls))
                                     )))

(defthm cmp-d-ls-induct-cmp-s-ls-induct-3-case1
    (implies (and (> i (+ j 1)) (dgl-p ls) (not (endp ls)) (natp i)
		  (natp j)
		  (>= (- i 1) (car ls))
		  (not (and (<= 0 (- (- i 1) (car ls)))
		       (<= (- (- i 1) (car ls)) 1 )))
		  (equal (cmp-d-ls-induct (- i 1) (cmp-s-ls-induct j (cdr ls)))
			 (cmp-s-ls-induct j (cmp-d-ls-induct (- i 2) (cdr ls)))
                                     )
		  )
             (equal (cmp-d-ls-induct i (cmp-s-ls-induct j ls))
		    (cmp-s-ls-induct j (cmp-d-ls-induct (- i 1) ls))
                                     ))
)



(defun cmp-d-ls-induct-4 (d ls)
  (declare (xargs :measure (len ls)))
   (cond 
	 ((endp ls) nil)
         ((< (- d 1) (car ls)) (cons (1- (car ls)) (cmp-d-ls-induct-4 d (cdr ls))))
         ((and (<= 0 (- (- d 1) (car ls)))
               (<= (- (- d 1) (car ls)) 1)) (cdr ls))              
         (t (cons (car ls) (cmp-d-ls-induct-4 (- d 1) (cdr ls))))
         )
   )

(defthm cmp-d-ls-induct-cmp-s-ls-induct-3
    (implies (and (> i (+ j 1)) (dgl-p ls) (natp i) (natp j))
             (equal (cmp-d-ls-induct i (cmp-s-ls-induct j ls))
		    (cmp-s-ls-induct j (cmp-d-ls-induct (- i 1) ls))
                    
))
:hints (("Goal" :induct (cmp-d-ls-induct-4 i ls)
))
)


(defthm cmp-d-ls-cmp-s-ls-prop5
  (implies (and (> i (+ j 1)) (dgl-p ls) (natp i) (natp j))
             (equal (cmp-d-ls i (cmp-s-ls j ls))
		    (cmp-s-ls j (cmp-d-ls (- i 1) ls))
                    
)))

(defun cmp-d-ls-do-induct (d ls)
  (declare (xargs :measure (len ls)))
   (cond 
	 ((endp ls) d)
         ((< (- d 1) (car ls)) (cmp-d-ls-do-induct d (cdr ls)))
         ((and (<= 0 (- (- d 1) (car ls)))
               (<= (- (- d 1) (car ls)) 1)) nil)              
         (t (cmp-d-ls-do-induct (- d 1) (cdr ls)))
         )
   )


;;;----------------------------------------------------------------------------
;;;
;;; face o face, i < j
;;; Property 1 of Simplicial Sets for degeneration lists 
;;;
;;;----------------------------------------------------------------------------

(defthm cmp-d-induct-cmp-d-induct-case-3.1.1
  (implies (and (< i j) (natp i) (natp j) (dgl-p ls) (not (endp ls))
		(< j (car ls))
		)
	   (equal (cmp-d-ls-induct (- j 1) (cmp-d-ls-induct i ls))
		  (cmp-d-ls-induct (- j 1) (cons (- (car ls) 1) (cmp-d-ls-induct i (cdr ls))))
		  ))
)

(defthm cmp-d-induct-cmp-d-induct-case-3.1
  (implies (and (< i j) (natp i) (natp j) (dgl-p ls) (not (endp ls))
		(< j (car ls))
		)
	   (equal (cmp-d-ls-induct (- j 1) (cmp-d-ls-induct i ls))
		  (cons (- (- (car ls) 1) 1) (cmp-d-ls-induct (- j 1) (cmp-d-ls-induct i (cdr ls))))
		  ))

)

(defthm cmp-d-induct-cmp-d-induct-case-3.2
  (implies (and (< i j) (natp i) (natp j) (dgl-p ls) (not (endp ls))
		(< j (car ls))
		)
	   (equal (cmp-d-ls-induct i (cmp-d-ls-induct j ls))
		  (cons (- (- (car ls) 1) 1) (cmp-d-ls-induct i (cmp-d-ls-induct j (cdr ls))))
		  ))
)


(defthm cmp-d-induct-cmp-d-induct-case-3
  (implies (and (< i j) (natp i) (natp j) (dgl-p ls) (not (endp ls))
		(< j (car ls))
		(equal (cmp-d-ls-induct (- j 1) (cmp-d-ls-induct i (cdr ls)))
		  (cmp-d-ls-induct i (cmp-d-ls-induct j (cdr ls)))
		  )
		)
	   (equal (cmp-d-ls-induct (- j 1) (cmp-d-ls-induct i ls))
		  (cmp-d-ls-induct i (cmp-d-ls-induct j ls))
		  ))
)



(defthm cmp-d-induct-cmp-d-induct-case-2.1
  (implies (and (< i j) (natp i) (natp j) (dgl-p ls) (not (endp ls))
		(>= j (car ls))
		(= j (car ls))
		)
	   (equal (cmp-d-ls-induct (- j 1) (cmp-d-ls-induct i ls))
		  (cmp-d-ls-induct i (cmp-d-ls-induct j ls))
		  ))
)

(defthm cmp-d-induct-cmp-d-induct-case-2.2.1
  (implies (and (< i j) (natp i) (natp j) (dgl-p ls) (not (endp ls))
		(>= j (car ls))
		(= j (+ (car ls) 1))
		(< i (car ls))
		)
	   (equal (cmp-d-ls-induct (- j 1) (cmp-d-ls-induct i ls))
		  (cmp-d-ls-induct i (cmp-d-ls-induct j ls))
		  ))
)


(defthm cmp-d-induct-cmp-d-induct-case-2.2.2-help
  (implies (and (< i j) (natp i) (natp j) (dgl-p ls) (not (endp ls))
		(>= j (car ls))
		(= j (+ (car ls) 1))
		(= i (car ls)))
	   (equal i (- j 1)))
:rule-classes nil
)

(defthm cmp-d-induct-cmp-d-induct-case-2.2.2.1
  (implies (and (< i j) (natp i) (natp j) (dgl-p ls) (not (endp ls))
		(>= j (car ls))
		(= j (+ (car ls) 1))
		(= i (car ls))
		)
	   (equal (cmp-d-ls-induct (- j 1) (cmp-d-ls-induct i ls))
		  (cmp-d-ls-induct (- j 1) (cdr ls))
		  ))
)

(defthm cmp-d-induct-cmp-d-induct-case-2.2.2.2
  (implies (and (< i j) (natp i) (natp j) (dgl-p ls) (not (endp ls))
		(>= j (car ls))
		(= j (+ (car ls) 1))
		(= i (car ls))
		)
	   (equal (cmp-d-ls-induct i (cmp-d-ls-induct j ls))
		  (cmp-d-ls-induct i (cdr ls))
		  ))
)


(defthm cmp-d-induct-cmp-d-induct-case-2.2.2
  (implies (and (< i j) (natp i) (natp j) (dgl-p ls) (not (endp ls))
		(>= j (car ls))
		(= j (+ (car ls) 1))
		(= i (car ls))
		)
	   (equal (cmp-d-ls-induct (- j 1) (cmp-d-ls-induct i ls))
		  (cmp-d-ls-induct i (cmp-d-ls-induct j ls))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance cmp-d-induct-cmp-d-induct-case-2.2.2.1
			  (i i) (j j) (ls ls))
	       (:instance cmp-d-induct-cmp-d-induct-case-2.2.2.2
			  (i i) (j j) (ls ls))
	       (:instance cmp-d-induct-cmp-d-induct-case-2.2.2-help
			  (i i) (j j) (ls ls))
	       )
	 
))
)




(defthm cmp-d-induct-cmp-d-induct-case-2.2-help
  (implies (and (< i j) (natp i) (natp j) (dgl-p ls) (not (endp ls))
		(>= j (car ls))
		(= j (+ (car ls) 1))
		)
	   (or (< i (car ls))
	       (= i (car ls))))
:rule-classes nil
)

(defthm cmp-d-induct-cmp-d-induct-case-2.2
  (implies (and (< i j) (natp i) (natp j) (dgl-p ls) (not (endp ls))
		(>= j (car ls))
		(= j (+ (car ls) 1))
		)
	   (equal (cmp-d-ls-induct (- j 1) (cmp-d-ls-induct i ls))
		  (cmp-d-ls-induct i (cmp-d-ls-induct j ls))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance cmp-d-induct-cmp-d-induct-case-2.2-help
			  (i i) (j j) (ls ls))
	       (:instance cmp-d-induct-cmp-d-induct-case-2.2.2
			  (i i) (j j) (ls ls))
	       (:instance cmp-d-induct-cmp-d-induct-case-2.2.1
			  (i i) (j j) (ls ls))
	       )))
)

(defthm cmp-d-induct-cmp-d-induct-case-2-help
  (implies (and (< i j) (natp i) (natp j) (dgl-p ls) (not (endp ls))
		(>= j (car ls))
		(and (<= 0 (- j (car ls)))
		     (<= (- j (car ls)) 1))
		)
	   (or (= j (car ls))
	       (= j (+ (car ls) 1))))
:rule-classes nil
)

(defthm cmp-d-induct-cmp-d-induct-case-2
  (implies (and (< i j) (natp i) (natp j) (dgl-p ls) (not (endp ls))
		(>= j (car ls))
		(and (<= 0 (- j (car ls)))
		     (<= (- j (car ls)) 1))
		)
	   (equal (cmp-d-ls-induct (- j 1) (cmp-d-ls-induct i ls))
		  (cmp-d-ls-induct i (cmp-d-ls-induct j ls))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance cmp-d-induct-cmp-d-induct-case-2-help
			  (i i) (j j) (ls ls))
	       (:instance cmp-d-induct-cmp-d-induct-case-2.2
			  (i i) (j j) (ls ls))
	       (:instance cmp-d-induct-cmp-d-induct-case-2.1
			  (i i) (j j) (ls ls))
	       )))
)


(defthm cmp-d-induct-cmp-d-induct-case-1
  (implies (and (< i j) (natp i) (natp j) (dgl-p ls) (not (endp ls))
		(>= j (car ls))
		(not (and (<= 0 (- j (car ls)))
		     (<= (- j (car ls)) 1)))
		(equal (cmp-d-ls-induct (- (- j 1) 1) (cmp-d-ls-induct i (cdr ls)))
		  (cmp-d-ls-induct i (cmp-d-ls-induct (- j 1) (cdr ls)))
		  )
		)
	   (equal (cmp-d-ls-induct (- j 1) (cmp-d-ls-induct i ls))
		  (cmp-d-ls-induct i (cmp-d-ls-induct j ls))
		  ))
)


(defthm cmp-d-ls-induct-cmp-d-ls-induct-property-1
    (implies (and (< i j) (natp i) (natp j) (dgl-p ls))
             (equal (cmp-d-ls-induct (- j 1) (cmp-d-ls-induct i ls))
		    (cmp-d-ls-induct i (cmp-d-ls-induct j ls))
                    ))
:HINTS (("Goal" :INDUCT (CMP-D-LS-INDUCT J LS)))
)
	

(defthm cmp-d-ls-cmp-d-ls
    (implies (and (< i j) (natp i) (natp j) (dgl-p ls))
             (equal (cmp-d-ls (- j 1) (cmp-d-ls i ls))
		    (cmp-d-ls i (cmp-d-ls j ls))
                    )))


;;;----------------------------------------------------------------------------
;;;
;;; My-member definitions and properties
;;;
;;;----------------------------------------------------------------------------

(defun my-member (i ls)
  (if (endp ls)
      nil
    (if (and (<= 0 (- i (car ls)))
	     (<= (- i (car ls)) 1))
	t
      (my-member i (cdr ls)))))



(defun my-member-2 (i ls)
  (if (endp ls)
      nil
    (if (= 0 (- i (car ls)))
	t
      (my-member-2 i (cdr ls)))))

(defun my-member-3 (i ls)
  (if (endp ls)
      nil
    (if (= 1 (- i (car ls)))
	t
      (my-member-3 i (cdr ls)))))

(defthm my-member-1-implies-my-member-2
  (implies (and (natp i)
		(dgl-p ls)
		(my-member i ls))
	   (or (my-member-2 i ls)
	       (my-member-3 i ls)))
:rule-classes nil
)


(defthm my-member-1-implies-my-member-2-b
  (implies (and (natp i)
		(dgl-p ls)
		)
	   (equal (my-member-2 i ls)
		  (my-member-3 (+ i 1) ls)
	   )))


(defthm my-member-implies-face-do-null 
  (implies (and (natp i)
		(dgl-p ls)
		(my-member i ls))
	   (null (cmp-d-ls-d-do i ls)))
:hints (("Goal" :induct (cmp-d-ls-d-do i ls)
))
)

(defthm not-my-member-implies-face-do-not-null 
  (implies (and (natp i)
		(dgl-p ls)
		(not (my-member i ls)))
	   (cmp-d-ls-d-do i ls))
:hints (("Goal" :induct (cmp-d-ls-d-do i ls)
))
)

(defthm face-do-null-implies-not-my-member
  (implies (and (natp i)
		(dgl-p ls)
		(cmp-d-ls-d-do i ls)
		)
	   (not (my-member i ls)))
:hints (("Goal" :induct (cmp-d-ls-d-do i ls)
))
)

(defthm face-do-if-null-implies-not-my-member
  (implies (and (natp i)
		(dgl-p ls)
		(null (cmp-d-ls-d-do i ls))
		)
	   (my-member i ls))
:hints (("Goal" :induct (cmp-d-ls-d-do i ls)))
)

;;;----------------------------------------------------------------------------
;;;
;;; Theorems for Property 2
;;;
;;;----------------------------------------------------------------------------

;;; The only theorem needed is cmp-s-ls-property

;;;----------------------------------------------------------------------------
;;;
;;; Theorems for Property 3
;;;
;;;----------------------------------------------------------------------------


(defthm i<j=>cmp-d-ls-d-do-i-cmp-s-ls-j=cmp-d-ls-d-do-i
  (implies (< i j)
	   (equal (cmp-d-ls-d-do i (cmp-s-ls j dgop))
		  (cmp-d-ls-d-do i dgop))))


;;;----------------------------------------------------------------------------
;;;
;;; Theorems for Property 4
;;;
;;;----------------------------------------------------------------------------

(defthm i=>nullcmp-d-ls-d-do-i-cmp-s-ls-i
  (implies (natp i)
	   (null (cmp-d-ls-d-do i (cmp-s-ls i dgop)))))

(defthm i=>nullcmp-d-ls-d-do-1+i-cmp-s-ls-i
  (implies (natp i)
	   (null (cmp-d-ls-d-do (1+ i) (cmp-s-ls i dgop)))))


;;;----------------------------------------------------------------------------
;;;
;;; Theorems for Property 5
;;;
;;;----------------------------------------------------------------------------


(defthm face-null-implies-deg-face-null
  (implies (and (> i (+ j 1)) (dgl-p ls) (natp i) (natp j)
		(null (cmp-d-ls-d-do (- i 1) ls)))
	   (null (cmp-d-ls-d-do i (cmp-s-ls j ls))))
:hints (("Goal" :induct (cmp-d-ls-do-induct i ls)
)))


(defthm face-not-null-implies-deg-face-not-null
    (implies (and (< i j)
                  (dgl-p ls)
                  (not (null (cmp-d-ls-d-do i ls))))
             (not (null (cmp-d-ls-d-do i (cmp-s-ls j ls))))))


(defthm face-not-null-implies-deg-face-not-null-to-prop5
  (implies (and (> i (+ j 1)) (dgl-p ls) (natp i) (natp j)
		(not(null (cmp-d-ls-d-do (- i 1) ls))))
	   (not (null (cmp-d-ls-d-do i (cmp-s-ls j ls)))))
:hints (("Goal" :induct (cmp-d-ls-do-induct i ls)
)))


(defthm i>j+1=>cmp-d-ls-d-do-i-cmp-s-ls-j=cmp-d-ls-d-do-i-1
  (implies (and (> i (+ j 1)) (natp i) (natp j)
		(not(null (cmp-d-ls-d-do (- i 1) dgop))))
	   (equal (cmp-d-ls-d-do (- i 1) dgop)
		  (cmp-d-ls-d-do i (cmp-s-ls j dgop))
		  ))
:hints (("Goal" :induct (cmp-d-ls-do-induct i dgop)
)))

(defthm i>j+1=>cmp-d-ls-d-do-i-cmp-s-ls-j=cmp-d-ls-d-do-i-1-bis
  (implies (and (> i (+ j 1)) (natp i) (natp j)
		(not(null (cmp-d-ls-d-do (- i 1) dgop))))
	   (equal (cmp-d-ls-d-do i (cmp-s-ls j dgop))
		  (cmp-d-ls-d-do (- i 1) dgop)
		  ))
:hints (("Goal" :induct (cmp-d-ls-do-induct i dgop)
)))

;;;----------------------------------------------------------------------------
;;;
;;; Theorems for Property 1
;;;
;;;----------------------------------------------------------------------------


;; Four cases are considered

;; First case:
;;-> (null (cmp-d-ls-d-do j ls))
;;-> (null (cmp-d-ls-d-do i ls))

;; Two cases are considered:

;; First case:
;; i<j-1

(defthm lemma1
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(> (- j 1) i)
		)
	   (my-member i (cmp-d-ls j ls))
	   )
)

(defthm lemma1-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))		
		(> j i)
		(> (- j 1) i)
		)
	   (null (cmp-d-ls-d-do i (cmp-d-ls j ls)))
	   )
 :hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma1)
		 (:instance dgl-p-cmp-d-ls (n j) (dgl ls))
		 (:instance my-member-implies-face-do-null
			    (ls (cmp-d-ls j ls)))
		 )))
)

(defthm lemma2
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(> (- j 1) i))
	   (my-member (- j 1) (cmp-d-ls i ls))
	   )
)


(defthm lemma2-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))		
		(> j i)
		(> (- j 1) i)
		)
	   (null (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls)))
	   )
 :hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma2)
		 (:instance dgl-p-cmp-d-ls (n i) (dgl ls))
		 (:instance my-member-implies-face-do-null (i (- j 1))
			    (ls (cmp-d-ls i ls)))
		 )))
)

;; Second case
;; i=j-1

;; Eight cases are considered

;; First case:
;; i \in ls, i+1 \not\in ls, i-1 \not\in ls

(defthm lemma1.0
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(= (- j 1) i)
		(not (my-member-2 j ls))
		(my-member-2 i ls)
		(not (my-member-3 i ls))
		)
	   (not (my-member i (cmp-d-ls j ls)))	   
	   )
)

(defthm lemma1.0-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(not (my-member-2 j ls))
		(my-member-2 i ls)
		(not (my-member-3 i ls))
		)
	   (cmp-d-ls-d-do i (cmp-d-ls j ls)))
:hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma1.0)
		 (:instance dgl-p-cmp-d-ls (n j) (dgl ls))
		 (:instance not-my-member-implies-face-do-not-null
			    (ls (cmp-d-ls j ls)))
		 )))	   
	   )


(defthm lemma2.0
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(= (- j 1) i)
		(not (my-member-2 j ls))
		(my-member-2 i ls)
		(not (my-member-3 i ls))
		)
	   (not (my-member (- j 1) (cmp-d-ls i ls)))	   
	   )
)

(defthm lemma2.0-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(not (my-member-2 j ls))
		(my-member-2 i ls)
		(not (my-member-3 i ls))
		)
	   (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls)))
:hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma2.0)
		 (:instance dgl-p-cmp-d-ls (n i) (dgl ls))
		 (:instance not-my-member-implies-face-do-not-null (i (- j 1))
			    (ls (cmp-d-ls j ls)))
		 )))	   
	   )


(defthm lemma1.0-lemma2.0-a
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(not (my-member-2 j ls))
		(my-member-2 i ls)
		(not (my-member-3 i ls))
		)
	   (equal
	    (cmp-d-ls-d-do i (cmp-d-ls j ls))
	    (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls)))))


;; Second case:
;; i \not\in ls, i+1 \in ls, i-1 \in ls

(defthm lemma1.1
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(not (my-member-2 i ls))
		(my-member-3 i ls)
		)
	   (my-member i (cmp-d-ls j ls))	   
	   )
)

(defthm lemma1.1-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(not (my-member-2 i ls))
		(my-member-3 i ls)
		)
	   (null (cmp-d-ls-d-do i (cmp-d-ls j ls))))
:hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma1.1)
		 (:instance dgl-p-cmp-d-ls (n j) (dgl ls))
		 (:instance my-member-implies-face-do-null
			    (ls (cmp-d-ls j ls)))
		 )))	   
	   )


(defthm lemma2.1
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(not (my-member-2 i ls))
		(my-member-3 i ls)
		)
	   (my-member (- j 1) (cmp-d-ls i ls))	   
	   )
)

(defthm lemma2.1-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(not (my-member-2 i ls))
		(my-member-3 i ls)
		)
	   (null (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls))))
:hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma2.1)
		 (:instance dgl-p-cmp-d-ls (n i) (dgl ls))
		 (:instance my-member-implies-face-do-null (i (- j 1))
			    (ls (cmp-d-ls j ls)))
		 )))	   
	   )


;; Third case:
;; i \in ls, i+1 \in ls, i-1 \not\in ls


(defthm lemma1.2
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(my-member-2 i ls)
		(not(my-member-3 i ls))
		)
	   (my-member i (cmp-d-ls j ls))	   
	   )
)

(defthm lemma1.2-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(my-member-2 i ls)
		(not(my-member-3 i ls))
		)
	   (null (cmp-d-ls-d-do i (cmp-d-ls j ls))))
:hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma1.2)
		 (:instance dgl-p-cmp-d-ls (n j) (dgl ls))
		 (:instance my-member-implies-face-do-null
			    (ls (cmp-d-ls j ls)))
		 )))	   
	   )


(defthm lemma2.2
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(my-member-2 i ls)
		(not(my-member-3 i ls))
		)
	   (my-member (- j 1) (cmp-d-ls i ls))	   
	   )
)

(defthm lemma2.2-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(my-member-2 i ls)
		(not(my-member-3 i ls))
		)
	   (null (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls))))
:hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma2.2)
		 (:instance dgl-p-cmp-d-ls (n i) (dgl ls))
		 (:instance my-member-implies-face-do-null (i (- j 1))
			    (ls (cmp-d-ls j ls)))
		 )))	   
	   )

;; Fourth case:
;; i \in ls, i+1 \not\in ls, i-1 \in ls


(defthm lemma1.3
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(= (- j 1) i)
		(not (my-member-2 j ls))
		(my-member-2 i ls)
		(my-member-3 i ls)
		)
	   (my-member i (cmp-d-ls j ls))	   
	   )
)

(defthm lemma1.3-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(not (my-member-2 j ls))
		(my-member-2 i ls)
		(my-member-3 i ls)
		)
	   (null (cmp-d-ls-d-do i (cmp-d-ls j ls))))
:hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma1.3)
		 (:instance dgl-p-cmp-d-ls (n j) (dgl ls))
		 (:instance my-member-implies-face-do-null
			    (ls (cmp-d-ls j ls)))
		 )))	   
	   )


(defthm lemma2.3
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(= (- j 1) i)
		(not (my-member-2 j ls))
		(my-member-2 i ls)
		(my-member-3 i ls)
		)
	   (my-member (- j 1) (cmp-d-ls i ls))	   
	   )
)

(defthm lemma2.3-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(not (my-member-2 j ls))
		(my-member-2 i ls)
		(my-member-3 i ls)	
		)
	   (null (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls))))
:hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma2.3)
		 (:instance dgl-p-cmp-d-ls (n i) (dgl ls))
		 (:instance my-member-implies-face-do-null (i (- j 1))
			    (ls (cmp-d-ls j ls)))
		 )))	   
	   )



;; Fifth case:
;; i \in ls, i+1 \in ls, i-1 \in ls


(defthm lemma1.4
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(my-member-2 i ls)
		(my-member-3 i ls)
		)
	   (my-member i (cmp-d-ls j ls))	   
	   )
)

(defthm lemma1.4-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(my-member-2 i ls)
		(my-member-3 i ls)
		)
	   (null (cmp-d-ls-d-do i (cmp-d-ls j ls))))
:hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma1.4)
		 (:instance dgl-p-cmp-d-ls (n j) (dgl ls))
		 (:instance my-member-implies-face-do-null
			    (ls (cmp-d-ls j ls)))
		 )))	   
	   )


(defthm lemma2.4
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(my-member i ls)
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(my-member-2 i ls)
		(my-member-3 i ls)
		)
	   (my-member (- j 1) (cmp-d-ls i ls))	   
	   )
)

(defthm lemma2.4-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(null (cmp-d-ls-d-do i ls))
		(> j i)
		(= (- j 1) i)
		(my-member-2 j ls)
		(my-member-2 i ls)
		(my-member-3 i ls)	
		)
	   (null (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls))))
:hints (("Goal" :do-not-induct t
	   :use ((:instance my-member-implies-face-do-null (i j))
		 (:instance my-member-implies-face-do-null (i i))
		 (:instance lemma2.4)
		 (:instance dgl-p-cmp-d-ls (n i) (dgl ls))
		 (:instance my-member-implies-face-do-null (i (- j 1))
			    (ls (cmp-d-ls j ls)))
		 )))	   
	   )

;; Sixth case:
;; i \not\in ls, i+1 \in ls, i-1 \not\in ls
;; Contradiction
;; Seventh case:
;; i \not\in ls, i+1 \not\in ls, i-1 \in ls
;; Contradiction
;; Eighth case:
;; i \not\in ls, i+1 \not\in ls, i-1 \not\in ls
;; Contradiction

(defthm case/6-help
  (implies (and (natp i) (dgl-p ls)
		(not (my-member-2 i ls))
		(not (my-member-3 i ls)))
	   (not (my-member i ls))))

(defthm case/8-help
  (implies (and (natp j) (dgl-p ls)
		(not (my-member-2 j ls))
		(not (my-member-2 (- j 1) ls)))
	   (not (my-member j ls)))
)




;; Second case:
;;-> (cmp-d-ls-d-do j ls)
;;-> (cmp-d-ls-d-do i ls)



(defthm lemma3
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(not (my-member j ls))
		(not (my-member i ls))
		(> j i))
	   (not (my-member (- j 1) (cmp-d-ls i ls)))
	   )
)



(defthm lemma3-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(cmp-d-ls-d-do j ls)
		(cmp-d-ls-d-do i ls)
		(> j i))
	   (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls)))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance face-do-null-implies-not-my-member (i j))
		 (:instance face-do-null-implies-not-my-member (i i))
		 (:instance lemma3)
		 (:instance dgl-p-cmp-d-ls (n i) (dgl ls))
		 (:instance not-my-member-implies-face-do-not-null (i (- j 1))
			    (ls (cmp-d-ls i ls)))
		 ))))

(defthm lemma11
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(cmp-d-ls-d-do j ls)
		(cmp-d-ls-d-do i ls)
		(> j i))
	   (equal (cmp-d-ls-d-do i ls)
		  (cmp-d-ls-d-do i (cmp-d-ls j ls) )
	    )
  ))

(in-theory (disable lemma11))

(defthm lemma4
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(not (my-member j ls))
		(not (my-member i ls))
		(> j i))
	   (not (my-member i (cmp-d-ls j ls)))
	   )
)


(defthm lemma4-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(cmp-d-ls-d-do j ls)
		(cmp-d-ls-d-do i ls)
		(> j i))
	   (cmp-d-ls-d-do i (cmp-d-ls j ls)))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance face-do-null-implies-not-my-member (i j))
		 (:instance face-do-null-implies-not-my-member (i i))
		 (:instance lemma4)
		 (:instance dgl-p-cmp-d-ls (n j) (dgl ls))
		 (:instance not-my-member-implies-face-do-not-null
			    (ls (cmp-d-ls j ls)))
		 ))))


(defthm lemma12.0
  (implies (and (natp j) (dgl-p ls)
		(> j (+ (car ls) 1))
		(> (- j 1) (+ (car ls) 1))
		(not (endp ls))
		) 
	   (equal (- (cmp-d-ls-d-do j ls) 1)
		  (cmp-d-ls-d-do (- j 1) (cmp-d-ls (- j 1) ls)
				 ))))


(defthm lemma12-1
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(cmp-d-ls-d-do j ls)
		(cmp-d-ls-d-do i ls)
		(> j i))
	   (< (cmp-d-ls-d-do i (cmp-d-ls j ls))
	      (cmp-d-ls-d-do j ls))
  )
:hints (("Goal" :induct (cmp-d-ls-d-do j ls))))



(defthm lemma12
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(cmp-d-ls-d-do j ls)
		(cmp-d-ls-d-do i ls)
		(> j i))
	   (equal (- (cmp-d-ls-d-do j ls) 1)
		  (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls) )   
	    )
  )
:hints (("Goal" :induct (cmp-d-ls-d-do j ls))))


;; Third case:
;;-> (null (cmp-d-ls-d-do j ls))
;;-> (cmp-d-ls-d-do i ls)

(defthm lemma5
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(my-member j ls)
		(not (my-member i ls))
		(> j i))
	   (my-member (- j 1) (cmp-d-ls i ls))))


(defthm lemma5-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(null (cmp-d-ls-d-do j ls))
		(cmp-d-ls-d-do i ls)
		(> j i))
	   (null (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance face-do-if-null-implies-not-my-member (i j))
		 (:instance face-do-null-implies-not-my-member (i i))
		 (:instance lemma5)
		 (:instance dgl-p-cmp-d-ls (n i) (dgl ls))
		 (:instance my-member-implies-face-do-null (i (- j 1))
			    (ls (cmp-d-ls i ls)))
		 ))))



(defthm lemma6-1
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(not (my-member i ls))
		(my-member j ls)
		(> j i)
		(< i (- j 1))
		)
	   (not (my-member i (cmp-d-ls j ls)))
	   )
)


(defthm lemma6-2
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(not (my-member i ls))
		(my-member j ls)
		(> j i)
		(= i (- j 1))
		)
	   (not (my-member i (cmp-d-ls j ls)))
	   )
)

(defthm lemma6
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(not (my-member i ls))
		(my-member j ls)
		(> j i)
		)
	   (not (my-member i (cmp-d-ls j ls)))
	   )
:hints (("Goal" :do-not-induct t
	 :use ((:instance lemma6-2)
	       (:instance lemma6-1))))
)

(defthm lemma6-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(cmp-d-ls-d-do i ls)
		(null (cmp-d-ls-d-do j ls))
		(> j i)
		)
	   (cmp-d-ls-d-do i (cmp-d-ls j ls) )
	   )
:hints (("Goal" :do-not-induct t
	 :use ((:instance face-do-if-null-implies-not-my-member (i j))
		 (:instance face-do-null-implies-not-my-member (i i))
		 (:instance lemma6)
		 (:instance dgl-p-cmp-d-ls (n j) (dgl ls))
		 (:instance not-my-member-implies-face-do-not-null
			    (ls (cmp-d-ls i ls)))
		 )))
)

(defthm lemma10
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(cmp-d-ls-d-do i ls)
		(null (cmp-d-ls-d-do j ls))
		(> j i)
		)
	   (equal (cmp-d-ls-d-do i (cmp-d-ls j ls) )
		  (cmp-d-ls-d-do i ls)
	   )
))


;; Fourth case:
;;-> (cmp-d-ls-d-do j ls)
;;-> (null (cmp-d-ls-d-do i ls))

(defthm lemma7
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(not (my-member j ls))
		(my-member i ls)
		(> j i))
	   (not (my-member (- j 1) (cmp-d-ls i ls)))))

(defthm lemma7-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(cmp-d-ls-d-do j ls)
		(null (cmp-d-ls-d-do i ls))
		(> j i))
	   (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls)))
:hints (("Goal" :do-not-induct t
	 :use ((:instance face-do-null-implies-not-my-member (i j))
		 (:instance face-do-if-null-implies-not-my-member (i i))
		 (:instance lemma7)
		 (:instance dgl-p-cmp-d-ls (n i) (dgl ls))
		 (:instance not-my-member-implies-face-do-not-null (i (- j 1))
			    (ls (cmp-d-ls i ls)))
		 ))))

(defthm lemma8
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(not (my-member j ls))
		(my-member i ls)
		(> j i))
	   (my-member i (cmp-d-ls j ls))))

(defthm lemma8-bis
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(cmp-d-ls-d-do j ls)
		(null (cmp-d-ls-d-do i ls))
		(> j i))
	   (null (cmp-d-ls-d-do i (cmp-d-ls j ls))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance face-do-null-implies-not-my-member (i j))
		 (:instance face-do-if-null-implies-not-my-member (i i))
		 (:instance lemma8)
		 (:instance dgl-p-cmp-d-ls (n j) (dgl ls))
		 (:instance my-member-implies-face-do-null
			    (ls (cmp-d-ls i ls)))
		 ))))

(defthm lemma9
  (implies (and (natp i)
		(natp j)
		(dgl-p ls)
		(cmp-d-ls-d-do j ls)
		(null (cmp-d-ls-d-do i ls))
		(> j i))
	   (equal (cmp-d-ls-d-do (- j 1) (cmp-d-ls i ls))
		  (cmp-d-ls-d-do j ls))))
